(*----------------------------------------------------------------------(C)-*)
(* Copyright (C) 2006 -2012 Konstantin Korovin and The University of Manchester.
This file is part of iProver - a theorem prover for first - order logic.

iProver is free software: you can redistribute it and / or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
iProver is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with iProver. If not, see < http:// www.gnu.org / licenses />. *)
(*----------------------------------------------------------------------[C]-*)

open Lib
open TermDB.Open

(*  subst.ml *)
type term = Term.term
type var = Var.var
module SMap = Symbol.Map
(*
let bot_term = Parser_types.bot_term
*)

type flat_subst = (var * term) list

(*type assignment = var*term*)
exception Subst_var_already_def

module SubstKey =
struct
	type t = var
	let compare = Var.compare
end

module SubstM = Map.Make (SubstKey)
type subst = term SubstM.t
let create() = SubstM.empty
let mem = SubstM.mem

let add v t subst =
	if mem v subst then raise Subst_var_already_def
	else SubstM.add v t subst

let find = SubstM.find
let remove = SubstM.remove
let map = SubstM.map
let fold = SubstM.fold
let iter = SubstM.iter

(* normalise var term by subst
we assume that there is no var cycles in subst *)

let rec find_normalised subst t =
	let x = Term.get_var t in
	try
		let x_val = (SubstM.find x subst) in
		if (Term.is_var x_val)
		then
			(try find_normalised subst x_val with
				Not_found -> x_val
			)
		else x_val
	(* match x_val with
	| Term.Var(v, _) ->
	(try find_normalised subst v with
	Not_found -> x_val
	)
	| _ -> x_val
	*)
	with
		Not_found -> t

type termDBref = TermDB.termDB ref
(* returns term in which all varibles in_term are replaced by by_term *)
(* and adds this term to termDB *)
(* we assume that  by_term and in_term are in term_db*)
(* non typed version *)
(*
let rec replace_vars term_db_ref by_term in_term =
if (Term.is_ground in_term) then in_term
else
match in_term with
| Term.Fun(sym, args, _) ->
let new_args =
Term.arg_map_left
(fun in_term' ->
(replace_vars term_db_ref by_term in_term')
) args in
let new_term = Term.create_fun_term_args sym new_args in
TermDB.add_ref new_term term_db_ref
| _ -> by_term
*)

(* by_term_map: maps vtypes -> terms ) *)
(* if there is no term in by_term_map then and default_term_opt = Some(default_term) then use default_term *)
(* if default term is None then do not instantiate this var *)
(* let replace_vars default_term_opt by_term_map in_term =
if (Term.is_ground in_term)
then in_term
else
begin
let f v =
let vtype = Var.get_type v in
(try
SMap.find vtype by_term_map
with Not_found ->
(match default_term_opt with
| Some default_term -> default_term
| None -> t
)
(* raise Type_of_var_is_not_in_map *)
)

in
Term.map f in_term
end
*)

let rec replace_vars default_term_opt by_term_map in_term =
	if (Term.is_ground in_term)
	then in_term
	else
		begin		
			match in_term with
			| Term.Fun(symb, args, _) ->
					Term.create_fun_term_args symb (Term.arg_map (replace_vars default_term_opt by_term_map) args)
			| Term.Var(v, _) ->
			
					let vtype = Var.get_type v in
					(try
						SMap.find vtype by_term_map
					with Not_found ->
							(match default_term_opt with
								| Some default_term -> default_term
								| None -> in_term
							)
					)
			(* raise Type_of_var_is_not_in_map *)
		end

let grounding term_db_ref by_term_map in_term =
	let bot_term = add_fun_term term_db_ref Symbol.symb_bot [] in
	let grounded =
		TermDB.add_ref (replace_vars (Some(bot_term)) by_term_map in_term) term_db_ref in
	Term.assign_grounding grounded in_term;
	grounded

(* applies substituion and adds obtained term into term_db *)
(* nothing is renamed, see substBound for this  *)
(* we assume that all terms in subst and t are in term_db *)
let rec apply_subst_term term_db_ref subst t =
	match t with
	| Term.Fun(sym, args, _) ->
			let new_args =
				Term.arg_map_left
					(fun t' ->
								apply_subst_term term_db_ref subst t'
					) args in
			let new_term = Term.create_fun_term_args sym new_args in
			TermDB.add_ref new_term term_db_ref
	| Term.Var(v, _) ->
			try
				SubstM.find v subst
			with
				Not_found -> t

let to_stream s subst =
	let item_to_str v t =
		(Term.to_stream s t);
		s.stream_add_char '/';
		(Var.to_stream s v);
		s.stream_add_str "; "
	in
	s.stream_add_char '[';
	iter item_to_str subst;
	s.stream_add_str "]\n"

let out = to_stream stdout_stream

let to_string =
	to_string_fun_from_to_stream_fun 30 to_stream

(*
let to_string subst =
let item_to_str v t rest =
rest^(Term.to_string t)^"/"^(Var.to_string v)^"; " in
"["^fold item_to_str subst ""^"]\n"
*)
